\begin{tabbing}
fischer\=\{\=\$x:ut2,\+\+
\\[0ex]\$try:ut2,
\\[0ex]\$taken:ut2,
\\[0ex]\$contending:ut2,
\\[0ex]\$free:ut2,
\\[0ex]\$mine:ut2,
\\[0ex]\$wanted:ut2,
\\[0ex]\$z:ut2\}
\-\\[0ex](${\it es}$; $L$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$e$:es{-}E(${\it es}$). \+
\\[0ex](es{-}loc(${\it es}$; $e$) $\in$ $L$ $\in$ Id)
\\[0ex]$\Rightarrow$ \=(es{-}dtype(${\it es}$; es{-}loc(${\it es}$; $e$); mkid\{\$x:ut2\}; Id)\+
\\[0ex]c$\wedge$ \=(\=((es{-}after(${\it es}$; mkid\{\$x:ut2\}; $e$) = mkid\{\$free:ut2\} $\in$ Id)\+\+
\\[0ex]$\vee$ (es{-}after(${\it es}$; mkid\{\$x:ut2\}; $e$) = mkid\{\$taken:ut2\} $\in$ Id)
\\[0ex]$\vee$ (es{-}after(${\it es}$; mkid\{\$x:ut2\}; $e$) = mkid\{\$mine:ut2\} $\in$ Id)
\\[0ex]$\vee$ (es{-}after(${\it es}$; mkid\{\$x:ut2\}; $e$) = mkid\{\$try:ut2\} $\in$ Id)
\\[0ex]$\vee$ (es{-}after(${\it es}$; mkid\{\$x:ut2\}; $e$) = mkid\{\$contending:ut2\} $\in$ Id))
\-\\[0ex]$\wedge$ (es{-}initially(${\it es}$; es{-}loc(${\it es}$; $e$); mkid\{\$x:ut2\}) = mkid\{\$free:ut2\} $\in$ Id)
\\[0ex]$\wedge$ \=(es{-}change{-}to(${\it es}$;Id;mkid\{\$x:ut2\};$e$;mkid\{\$try:ut2\})\+
\\[0ex]$\Rightarrow$ \=(((es{-}when(${\it es}$; mkid\{\$x:ut2\}; $e$) = mkid\{\$free:ut2\} $\in$ Id)\+
\\[0ex]$\vee$ (es{-}when(${\it es}$; mkid\{\$x:ut2\}; $e$) = mkid\{\$contending:ut2\} $\in$ Id))
\\[0ex]$\wedge$ l\_all(\=$L$;\+
\\[0ex]Id;
\\[0ex]$i$.(($\neg$($i$ = es{-}loc(${\it es}$; $e$) $\in$ Id))
\\[0ex]$\Rightarrow$ \=es{-}sends{-}on(${\it es}$;$e$;$<$es{-}loc(${\it es}$; $e$)\+
\\[0ex], $i$
\\[0ex], mkid\{\$z:ut2\}$>$;mkid\{\$wanted:ut2\})))))
\-\-\-\-\\[0ex]$\wedge$ \=(es{-}change{-}to(${\it es}$;Id;mkid\{\$x:ut2\};$e$;mkid\{\$mine:ut2\})\+
\\[0ex]$\Rightarrow$ (es{-}when(${\it es}$; mkid\{\$x:ut2\}; $e$) = mkid\{\$try:ut2\} $\in$ Id))
\-\\[0ex]$\wedge$ \=(es{-}change{-}to(${\it es}$;Id;mkid\{\$x:ut2\};$e$;mkid\{\$free:ut2\})\+
\\[0ex]$\Leftarrow\!\Rightarrow$ \=(((es{-}when(${\it es}$; mkid\{\$x:ut2\}; $e$) = mkid\{\$taken:ut2\} $\in$ Id)\+
\\[0ex]$\wedge$ \=(($\uparrow$es{-}isrcv(${\it es}$; $e$))\+
\\[0ex]c$\wedge$ \=((es{-}tag(${\it es}$; $e$) = mkid\{\$free:ut2\} $\in$ Id)\+
\\[0ex]$\wedge$ ($\exists$\=$i$:Id\+
\\[0ex](($i$ $\in$ $L$ $\in$ Id)
\\[0ex]$\wedge$ ($\neg$($i$ = es{-}loc(${\it es}$; $e$) $\in$ Id))
\\[0ex]$\wedge$ (\=es{-}lnk(${\it es}$; $e$)\+
\\[0ex]=
\\[0ex]$<$$i$, es{-}loc(${\it es}$; $e$), mkid\{\$z:ut2\}$>$
\\[0ex]$\in$ IdLnk))))))
\-\-\-\-\\[0ex]$\vee$ \=((es{-}when(${\it es}$; mkid\{\$x:ut2\}; $e$) = mkid\{\$mine:ut2\} $\in$ Id)\+
\\[0ex]$\wedge$ l\_all(\=$L$;\+
\\[0ex]Id;
\\[0ex]$i$.(($\neg$($i$ = es{-}loc(${\it es}$; $e$) $\in$ Id))
\\[0ex]$\Rightarrow$ \=es{-}sends{-}on(${\it es}$;$e$;$<$es{-}loc(${\it es}$; $e$)\+
\\[0ex], $i$
\\[0ex], mkid\{\$z:ut2\}$>$;mkid\{\$free:ut2\}))))))
\-\-\-\-\-\\[0ex]$\wedge$ \=(es{-}change{-}to(${\it es}$;Id;mkid\{\$x:ut2\};$e$;mkid\{\$contending:ut2\})\+
\\[0ex]$\Leftarrow\!\Rightarrow$ \=((es{-}when(${\it es}$; mkid\{\$x:ut2\}; $e$) = mkid\{\$try:ut2\} $\in$ Id)\+
\\[0ex]$\wedge$ \=(($\uparrow$es{-}isrcv(${\it es}$; $e$))\+
\\[0ex]c$\wedge$ \=((es{-}tag(${\it es}$; $e$) = mkid\{\$wanted:ut2\} $\in$ Id)\+
\\[0ex]$\wedge$ ($\exists$\=$i$:Id\+
\\[0ex](($i$ $\in$ $L$ $\in$ Id)
\\[0ex]$\wedge$ ($\neg$($i$ = es{-}loc(${\it es}$; $e$) $\in$ Id))
\\[0ex]$\wedge$ (\=es{-}lnk(${\it es}$; $e$)\+
\\[0ex]=
\\[0ex]$<$$i$, es{-}loc(${\it es}$; $e$), mkid\{\$z:ut2\}$>$
\\[0ex]$\in$ IdLnk)))))))
\-\-\-\-\-\-\\[0ex]$\wedge$ \=(es{-}change{-}to(${\it es}$;Id;mkid\{\$x:ut2\};$e$;mkid\{\$taken:ut2\})\+
\\[0ex]$\Rightarrow$ \=(((es{-}when(${\it es}$; mkid\{\$x:ut2\}; $e$) = mkid\{\$contending:ut2\} $\in$ Id)\+
\\[0ex]$\vee$ (es{-}when(${\it es}$; mkid\{\$x:ut2\}; $e$) = mkid\{\$free:ut2\} $\in$ Id))
\\[0ex]$\wedge$ \=(($\uparrow$es{-}isrcv(${\it es}$; $e$))\+
\\[0ex]c$\wedge$ \=((es{-}tag(${\it es}$; $e$) = mkid\{\$wanted:ut2\} $\in$ Id)\+
\\[0ex]$\wedge$ ($\exists$\=$i$:Id\+
\\[0ex](($i$ $\in$ $L$ $\in$ Id)
\\[0ex]$\wedge$ ($\neg$($i$ = es{-}loc(${\it es}$; $e$) $\in$ Id))
\\[0ex]$\wedge$ (\=es{-}lnk(${\it es}$; $e$)\+
\\[0ex]=
\\[0ex]$<$$i$, es{-}loc(${\it es}$; $e$), mkid\{\$z:ut2\}$>$
\\[0ex]$\in$ IdLnk)))))))
\-\-\-\-\-\-\\[0ex]$\wedge$ \=(($\uparrow$es{-}isrcv(${\it es}$; $e$))\+
\\[0ex]$\Rightarrow$ (es{-}tag(${\it es}$; $e$) = mkid\{\$free:ut2\} $\in$ Id)
\\[0ex]$\Rightarrow$ ($\exists$\=$i$:Id\+
\\[0ex](($i$ $\in$ $L$ $\in$ Id)
\\[0ex]$\wedge$ ($\neg$($i$ = es{-}loc(${\it es}$; $e$) $\in$ Id))
\\[0ex]$\wedge$ (es{-}lnk(${\it es}$; $e$) = $<$$i$, es{-}loc(${\it es}$; $e$), mkid\{\$z:ut2\}$>$ $\in$ IdLnk)))
\-\\[0ex]$\Rightarrow$ \=(subtype\_rel(\=es{-}vartype(${\it es}$; es{-}loc(${\it es}$; es{-}sender(${\it es}$; $e$)); mkid\{\$x:ut2\});\+\+
\\[0ex]Id)
\-\\[0ex]c$\wedge$ \=(es{-}change{-}to(${\it es}$;Id;mkid\{\$x:ut2\};es{-}sender(${\it es}$; $e$);mkid\{\$free:ut2\})\+
\\[0ex]$\wedge$ (\=es{-}when(${\it es}$; mkid\{\$x:ut2\}; es{-}sender(${\it es}$; $e$))\+
\\[0ex]=
\\[0ex]mkid\{\$mine:ut2\}
\\[0ex]$\in$ Id))))
\-\-\-\-\\[0ex]$\wedge$ \=(($\uparrow$es{-}isrcv(${\it es}$; $e$))\+
\\[0ex]$\Rightarrow$ (es{-}tag(${\it es}$; $e$) = mkid\{\$wanted:ut2\} $\in$ Id)
\\[0ex]$\Rightarrow$ ($\exists$\=$i$:Id\+
\\[0ex](($i$ $\in$ $L$ $\in$ Id)
\\[0ex]$\wedge$ ($\neg$($i$ = es{-}loc(${\it es}$; $e$) $\in$ Id))
\\[0ex]$\wedge$ (es{-}lnk(${\it es}$; $e$) = $<$$i$, es{-}loc(${\it es}$; $e$), mkid\{\$z:ut2\}$>$ $\in$ IdLnk)))
\-\\[0ex]$\Rightarrow$ \=(subtype\_rel(\=es{-}vartype(${\it es}$; es{-}loc(${\it es}$; es{-}sender(${\it es}$; $e$)); mkid\{\$x:ut2\});\+\+
\\[0ex]Id)
\-\\[0ex]c$\wedge$ es{-}change{-}to(${\it es}$;Id;mkid\{\$x:ut2\};es{-}sender(${\it es}$; $e$);mkid\{\$try:ut2\})))))
\-\-\-\-\-
\end{tabbing}